;;;===========================================================================
;;;
;;; Algebraic data structures 
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 02/06/10 || End date: /06/10
;;;
;;;===========================================================================

(in-package "ACL2")

(include-book "data-structures/structures" :dir :system)

(include-book "simplicial-algebraic-topology-macros")


;;;**************************************************
;;; Chain Complex Structure
;;;**************************************************

(defstructure chain-complex
  inv-ring addition-ring zero-element inverse product-ring unit
  inv-cc group-operation-cc zero-cc external-cc inverse-cc d-cc)


(defun check-chain-complex-aux (cc name hints)
  `(list 'defchain-complex
	(chain-complex-inv-ring ,cc) 
	(chain-complex-addition-ring ,cc) 
	(chain-complex-zero-element ,cc) 
	(chain-complex-inverse ,cc) 
	(chain-complex-product-ring ,cc) 
	(chain-complex-unit ,cc) 
	(chain-complex-inv-cc ,cc) 
	(chain-complex-group-operation-cc ,cc) 
	(chain-complex-zero-cc ,cc) 
	(chain-complex-external-cc ,cc) 
	(chain-complex-inverse-cc ,cc) 
	(chain-complex-d-cc ,cc) 
	,name
	:hints ,hints))


(defmacro check-chain-complex-p (cc name &key hints)
  (cons 'make-event 
	(cons (check-chain-complex-aux cc name hints) 'nil)))


;;;**************************************************
;;; Morphism degree 0
;;;**************************************************


(defstructure morphism-degree-0
  inv-source inv-target function group-operation-source group-operation-target 
  external-source external-target inv-ring
  zero-source zero-target inverse-source inverse-target
  )


(defun check-morphism-degree-0-aux (m name hints)
  `(list 'defmorphism-degree-0 
	(morphism-degree-0-inv-source ,m) 
	(morphism-degree-0-inv-target ,m) 
	(morphism-degree-0-function ,m) 
	(morphism-degree-0-group-operation-source ,m) 
	(morphism-degree-0-group-operation-target ,m)
	(morphism-degree-0-external-source ,m) 
	(morphism-degree-0-external-target ,m)
	(morphism-degree-0-inv-ring ,m)
	(morphism-degree-0-zero-source ,m) 
	(morphism-degree-0-zero-target ,m)
	(morphism-degree-0-inverse-source ,m) 
	(morphism-degree-0-inverse-target ,m)
	,name
	:hints ,hints))


(defmacro check-morphism-degree-0-p (m name &key hints)
  (cons 'make-event 
	(cons (check-morphism-degree-0-aux m name hints) 'nil)))



;;;**************************************************
;;; Morphism degree -1
;;;**************************************************

(defstructure morphism-degree--1
  inv-source inv-target function group-operation-source group-operation-target external-source external-target inv-ring
  zero-source zero-target inverse-source inverse-target  
  )


(defun check-morphism-degree--1-aux (m name hints)
  `(list 'defmorphism-degree--1 
	(morphism-degree--1-inv-source ,m) 
	(morphism-degree--1-inv-target ,m) 
	(morphism-degree--1-function ,m) 
	(morphism-degree--1-group-operation-source ,m) 
	(morphism-degree--1-group-operation-target ,m)
	(morphism-degree--1-external-source ,m) 
	(morphism-degree--1-external-target ,m)
	(morphism-degree--1-inv-ring ,m)
	(morphism-degree--1-zero-source ,m) 
	(morphism-degree--1-zero-target ,m)
	(morphism-degree--1-inverse-source ,m) 
	(morphism-degree--1-inverse-target ,m)
	,name
	:hints ,hints))


(defmacro check-morphism-degree--1-p (m name &key hints)
  (cons 'make-event 
	(cons (check-morphism-degree--1-aux m name hints) 'nil)))



;;;**************************************************
;;; Differential
;;;**************************************************

(defstructure differential
  inv function group-operation external inv-ring
  zero inverse
  )


(defun check-differential-aux (diff name hints)
  `(list 'defdifferential
	(differential-inv ,diff) 	 
	(differential-function ,diff) 
	(differential-group-operation ,diff) 	
	(differential-external ,diff) 	
	(differential-inv-ring ,diff)
	(differential-zero ,diff) 	
	(differential-inverse ,diff) 	
	,name
	:hints ,hints))


(defmacro check-differential-p (m name &key hints)
  (cons 'make-event 
	(cons (check-differential-aux m name hints) 'nil)))



;;;**************************************************
;;; Chain Complex Morphism degree 0 Structure
;;;**************************************************

(defstructure chain-complex-morphism-degree-0
  source-cc
  target-cc
  function 
  )



(defun check-chain-complex-morphism-degree-0-aux (ccm name hints)
  `(list 'defchain-complex-morphism-degree-0
	 (chain-complex-inv-ring (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-addition-ring (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-zero-element (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-inverse (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-product-ring (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-unit (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-inv-cc (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-group-operation-cc (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-zero-cc (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-external-cc (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-inverse-cc (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-d-cc (chain-complex-morphism-degree-0-source-cc ,ccm)) 
	 (chain-complex-inv-cc (chain-complex-morphism-degree-0-target-cc ,ccm)) 
	 (chain-complex-group-operation-cc (chain-complex-morphism-degree-0-target-cc ,ccm)) 
	 (chain-complex-zero-cc (chain-complex-morphism-degree-0-target-cc ,ccm)) 
	 (chain-complex-external-cc (chain-complex-morphism-degree-0-target-cc ,ccm)) 
	 (chain-complex-inverse-cc (chain-complex-morphism-degree-0-target-cc ,ccm)) 
	 (chain-complex-d-cc (chain-complex-morphism-degree-0-target-cc ,ccm)) 
	 (chain-complex-morphism-degree-0-function ,ccm)
	 ,name
	 :hints ,hints))


(defmacro check-chain-complex-morphism-degree-0-p (ccm name &key hints)
  (cons 'make-event 
	(cons (check-chain-complex-morphism-degree-0-aux ccm name hints) 'nil)))



;;;**************************************************
;;; Reduction
;;;**************************************************


(defstructure reduction
  top-cc
  bottom-cc
  f
  g
  h
  )


(defun check-reduction-aux (reduction name hints)
  `(list 'defreduction
	 (chain-complex-inv-ring (reduction-top-cc ,reduction)) 
	 (chain-complex-addition-ring (reduction-top-cc ,reduction)) 
	 (chain-complex-zero-element (reduction-top-cc ,reduction)) 
	 (chain-complex-inverse (reduction-top-cc ,reduction)) 
	 (chain-complex-product-ring (reduction-top-cc ,reduction)) 
	 (chain-complex-unit (reduction-top-cc ,reduction)) 
	 (chain-complex-inv-cc (reduction-top-cc ,reduction)) 
	 (chain-complex-group-operation-cc (reduction-top-cc ,reduction)) 
	 (chain-complex-zero-cc (reduction-top-cc ,reduction)) 
	 (chain-complex-external-cc (reduction-top-cc ,reduction)) 
	 (chain-complex-inverse-cc (reduction-top-cc ,reduction)) 
	 (chain-complex-d-cc (reduction-top-cc ,reduction)) 
	 (chain-complex-inv-cc (reduction-bottom-cc ,reduction)) 
	 (chain-complex-group-operation-cc (reduction-bottom-cc ,reduction)) 
	 (chain-complex-zero-cc (reduction-bottom-cc ,reduction)) 
	 (chain-complex-external-cc (reduction-bottom-cc ,reduction)) 
	 (chain-complex-inverse-cc (reduction-bottom-cc ,reduction)) 
	 (chain-complex-d-cc (reduction-bottom-cc ,reduction)) 
	 (reduction-f ,reduction)
	 (reduction-g ,reduction)
	 (reduction-h ,reduction)
	 ,name
	 :hints ,hints))


(defmacro check-reduction-p (reduction name &key hints)
  (cons 'make-event 
	(cons (check-reduction-aux reduction name hints) 'nil)))



;;;**************************************************
;;; Homotopy Equivalence
;;;**************************************************


(defstructure heq
  left-reduction
  right-reduction
  )


(defun check-heq-aux (heq name hints)
  `(list 'defhomotopy-equivalence 
	 (chain-complex-inv-ring (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-addition-ring (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-zero-element (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-inverse (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-product-ring (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-unit (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-inv-cc (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-group-operation-cc (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-zero-cc (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-external-cc (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-inverse-cc (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-d-cc (reduction-bottom-cc (heq-left-reduction ,heq))) 
	 (chain-complex-inv-cc (reduction-top-cc (heq-right-reduction ,heq))) 
	 (chain-complex-group-operation-cc (reduction-top-cc (heq-right-reduction ,heq))) 
	 (chain-complex-zero-cc (reduction-top-cc (heq-right-reduction ,heq))) 
	 (chain-complex-external-cc (reduction-top-cc (heq-right-reduction ,heq))) 
	 (chain-complex-inverse-cc (reduction-top-cc (heq-right-reduction ,heq))) 
	 (chain-complex-d-cc (reduction-top-cc (heq-right-reduction ,heq))) 
	 (chain-complex-inv-cc (reduction-bottom-cc (heq-right-reduction ,heq))) 
	 (chain-complex-group-operation-cc (reduction-bottom-cc (heq-right-reduction ,heq))) 
	 (chain-complex-zero-cc (reduction-bottom-cc (heq-right-reduction ,heq))) 
	 (chain-complex-external-cc (reduction-bottom-cc (heq-right-reduction ,heq))) 
	 (chain-complex-inverse-cc (reduction-bottom-cc (heq-right-reduction ,heq))) 
	 (chain-complex-d-cc (reduction-bottom-cc (heq-right-reduction ,heq)) ) 
	 (reduction-f (heq-left-reduction ,heq))
	 (reduction-g (heq-left-reduction ,heq))
	 (reduction-h (heq-left-reduction ,heq))
	 (reduction-f (heq-right-reduction ,heq))
	 (reduction-g (heq-right-reduction ,heq))
	 (reduction-h (heq-right-reduction ,heq))
	 ,name
	 :hints ,hints))


(defmacro check-heq-p (heq name &key hints)
  (cons 'make-event 
	(cons (check-heq-aux heq name hints) 'nil)))











